(set-option :produce-interpolants true)
(set-option :certify-interpolants 1)
(set-logic QF_UF)
(declare-sort Real 0)
(declare-fun g (Real Real ) Real)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun k () Real)

(assert (! (= x c) :named A1 ))
(assert (! (= y d) :named A2 ))
(assert (! (= a c) :named B1 ))
(assert (! (= b d) :named B2 ))
(assert (! (not (= (g x y) k)) :named A3 ))
(assert (! (= (g a b) k) :named B3))

(check-sat)
(get-interpolants (and A1 A2 A3)  (and B1 B2 B3))
